Nuprl Lemma : l_before_l_index 0,22
T:Type, dT:EqDecider(T), L:T List, x, y:T.
(x  L)  (y  L)  index(L;x)<index(L;y)  x before y  L 
latex

DefinitionsT, True, P  Q, P & Q, P  Q, x before y  l, Prop, index(L;x), P  Q, {i..j}, ||as||, (x  l), EqDecider(T), x:A. B(x), t  T
Lemmasdeq wf, l member wf, length wf1, int seg wf, l index wf, select l index, true wf, squash wf, l before wf, l before select

origin